package ch.epfl.lara.matcheck.verify;

import ch.epfl.lara.matcheck.ast.{Formula,Imply}
import ch.epfl.lara.matcheck.verify.axioms.IAxiom

/**
 * <p>
 *    The list of properties that we want to verify on a pattern matching expression.
 * </p>
 */
abstract class MatchProperties extends IAxiom  {
  
  /**
   * <p>
   *	Check that the pattern matching expression contains no two cases that are overlapping.
   *	If this is true then the different cases can be reorganized in any manner without 
   *	changing the final behaviour.
   * </p>
   *
   * @param axioms  : The axioms are retrieved from the class, object, method specification
   *		      and the userd-defined constraints. Before being used their 
   *		      truth is verified.
   * @param patterns: Patterns of the PM expr that have already been translated into formulae.
   * @return        : A formula for proving that disjointness of patterns hold. 
   */
  protected def disjoint(axiom: Axiom, patterns: List[Imply]): Formula 
  
  /**
   * <p>
   *    Check that the pattern matching expression is complete, that is there exist no
   *	mising cases. 
   *    If this is true then we can ensure that no <code>MatchError exception</code> are
   *	thrown during the execution (if we don't consider creation of new classes at run-time).
   * </p>
   *
   * @param axioms  : The axioms are retrieved from the class, object, method specification
   *                  and the userd-defined constraints. Before being used their 
   *                  truth is verified.
   * @param patterns: Patterns of the PM expr that have already been translated into formulae.
   * @return        : A formula for proving that completeness of patterns hold. 
   */
  protected def complete(axiom: Axiom, patterns: List[Imply]): Formula 
  
  /**
   * <p>
   *    Check that the pattern matching expression contains no unracheable closes, that is
   * 	there exist no case that will never be attained because it is already covered by 
   *    their predecessors.
   *    If this is false, then there is no dead code (but this clearly 
   *	doesn't imply that the PM is complete).
   * </p>
   *
   * @param axioms  : The axioms are retrieved from the class, object, method specification
   *                  and the userd-defined constraints. Before being used their 
   *                  truth is verified.
   * @param patterns: Patterns of the PM expr that have already been translated into formulae.
   * @return        : A formula for proving whether or not there is some dead code. 
   */
  protected def unreachable(axiom: Axiom, patterns: List[Imply]): List[Formula]

}
